T:Type, as:(T List), n:{0...||as||}, i:{0..(||as|| - n)}. nth_tl(n;as)[i] = as[(i+n)]  T 

latex

ProofTree

Definitions	t  T, Y, ||as||, x:A. B(x), T, ff, P  Q, P & Q, P  Q, tt, P  Q, tl(l), if b then t else f fi , nth_tl(n;as), True, , S  T, {i...j}, Unit, , False, A, i  j < k, A  B, {i..j},
Lemmas	int iseg wf, int seg wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity, length wf1, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf, add functionality wrt eq, non neg length, length cons, select wf, select cons tl